r:Rng, u, v:|r|, b:. (u * (when b. v)) = (when b. (u * v))  |r| 

latex

Definitions	x:A. B(x), when b. p, when b. p, r+gp, if b t else f fi, e, t  T, true, false, 1of(t), 2of(t), x f y, P  Q, P  Q, P & Q, P  Q, Rng, , Unit,
Lemmas	bool wf, rng car wf, rng wf, rng times wf, rng times zero, rng zero wf